$\forall$$a$:Atom1, $T$:Type, $g$:($T$$\rightarrow\mathbb{B}$), $x$:$T$. AtomFree(Type;$T$) $\Rightarrow$ M($a$;$g$;$x$) $\in$ $\mathbb{B}$